TelescopingLet2.agda:4,9-10
Not in scope:
  ★
  at TelescopingLet2.agda:4,9-10
when scope checking ★
